<HR><!------------------------------------------------------------------------>
<H2>E&nbsp;0.82 and EP&nbsp;0.82</H2>
S. Schulz<BR>
Institut f&uuml;r Informatik, Technische Universit&auml;t
M&uuml;nchen, Germany, and ITC/irst, Trento, Italy
<BR>schulz@informatik.tu-muenchen.de<p>

<H3>Architecture</H3>

E&nbsp;0.82[<A HREF="#References">Sch2002,Sch2004</A>] is a purely
equational theorem prover. The core proof procedure operates on
formulas in clause normal form, using a calculus that combines
superposition (with selection of negative literals) and rewriting. No
special rules for non-equational literals have been implemented,
i.e., resolution is simulated via paramodulation and equality
resolution. The basic calculus is extended with rules for AC
redundancy elemination, some contextual simplification, and
pseudo-splitting. 
<p>
E is based on the DISCOUNT-loop variant of the <em>given-clause</em>
algorithm, i.e. a strict separation of active and passive facts.
Proof search in E is primarily controlled by a literal selection
strategy, a clause evaluation heuristic, and a simplification
ordering. The prover supports a large number of preprogrammed literal
selection strategies, many of which are only experimental. Clause
evaluation heuristics can be constructed on the fly by combining
various parameterized primitive evaluation functions, or can be
selected from a set of predefined heuristics. Supported term orderings
are several parameterized instances of Knuth-Bendix-Ordering (KBO) and
Lexicographic Path Ordering (LPO).
<p>
E uses a preprocessing step to convert formulas in full first order
format to clause normal form. Preprocessing also unfolds equational
definitions and performs some simplifications on the clause level.
<p>
The automatic mode can selects literal selection strategy, term
ordering, and search heuristic based on simple problem characteristics
of the preprocessed clausal problem. 
<p>
EP&nbsp;0.82 is just a combination of E&nbsp;0.82 in verbose mode and
a proof analysis tool extracting the used inference steps.
<p>


<H3>Implementation</H3>

E is implemented in ANSI C, using the GNU C compiler. The most
outstanding feature is the global sharing of rewrite steps. Current
versions of E add <em>rewrite
links</em> from rewritten to new terms. In effect, E is caching
rewrite operations as long as sufficient memory is available. Other
important features are the use of <EM>perfect discrimination trees</EM>
with age and size constraints for rewriting and unit-subsumption,
<em>feature vector indexing</em>[<A HREF="#References">Sch2004b</A>]
for forward- and backward subsumption and contextual literal cutting,
and a new polynomial implementation of LPO[<A
HREF="#References">Loe2004</A>].
<P>
The program has been successfully installed under SunOS&nbsp;4.3.x,
Solaris&nbsp;2.x, HP-UX&nbsp;B&nbsp;10.20, MacOS-X, and various
versions of Linux.  Sources of the latest released version are
available freely from: 
<PRE>
    <A HREF="http://www.eprover.org">http://www.eprover.org</A>
</PRE>
EP&nbsp;0.82 is a simple Bourne shell script calling E and the postprocessor in
a pipeline.

<h3>Strategies</h3>

E's automatic mode is optimized for performance on TPTP 2.6.0. The
optimization is based on about 90 test runs over the library (and
previous experience) and consists of the selection of one of about 50
different strategies for each problem. All test runs have been
performed on SUN Ultra 60/300 machines with a time limit of 300
seconds (or roughly equivalent configurations). All individual
strategies are general purpose, the worst one solves about 49% of TPTP
2.6.0, the best one about 60%.

E distinguishes problem classes based on a number of features, all of
which have between two and 4 possible  values. The most important ones
are:
<ul>
<li> Is the most general non-negative clause unit, Horn, or Non-Horn?
<li> Is the most general negative clauce unit or non-unit?
<li> Are all negative clauses unit clauses?
<li> Are all literals equality literals, are some literas equality
     literals, or is the problem non-equational?
<li> Are there a few, some, or many clauses in the problem?
<li> Is the maximum arity of any function symbol 0, 1, 2, or greater? 
<li> Is the sum of function symbol arities in the signature small,
     medium, or large?
</ul>

Wherever there is a three-way split on a numerical feature value,
the limits are selected automatically with the aim of
splitting the set of problems into approximately equal
sized parts based on this one feature.

<p>
For classes above a threshold size, we assign the absolute best
heuristic to the class. For smaller, non-empty classes, we assign the
globally best heuristic that solves the same number of problems on
this class as the best heuristic on this class does. Empty classes are
assigned the globally best heuristic. Typically, most selected
heuristics are assigned to more than one class.


<H3>Expected Competition Performance</H3>

In the last year, E performed well in the MIX category of CASC and
came in third in the UEQ division. We believe that E will again be
among the strongest provers in the MIX category, in particular due to
its good performance for Horn problems. In UEQ, E will probably be
beaten only by Waldmeister, and, possibly, E-SETHEO (which
incorporates it). We cannot predict performance on FOF problems yet,
but hope that E will be competitive.
<p>
EP&nbsp;0.82 will be hampered by the fact that it has to analyse the
inference step listing, an operation that typically is about as
expensive as the proof search itself. Nevertheless, it should be
competitive among the MIX* and FOF* systems.
<p>


<A NAME="References">
<H3>References</H3>
<DL>
<DT> Sch2002
<DD> Schulz S. (2002),
     <STRONG>E: A Brainiac Theorem Prover</STRONG>,
     <EM>Journal of AI Communications</em> 15(2/3), 111-126, IOS Press
<DT> Sch2004
<DD> Schulz S. (2004),
     <STRONG>System Abstract: E 0.81</STRONG>,
     <EM>Proceedings of the 3rd IJCAR</EM>,
     (Cork, Ireland),
     Lecture Notes in Artificial Intelligence,
     Springer-Verlag
<DT> Sch2004b
<DD> Schulz S. (2004),
     <STRONG>Simple and Efficient Clause Subsumption with Feature
     Vector Indexing</STRONG>,
     <EM>Proceedings of the IJCAR-2004 Workshop on Empirically
     Successful First-Order Theorem Proving</EM>, (Cork, Ireland),
     ENTCS, Elsevier Science
<DT> Loe2004
<DD> L&ouml;chner b. (2004),
     <STRONG>What to know when implementing LPO</STRONG>,
     <EM>Proceedings of the IJCAR-2004 Workshop on Empirically
     Successful First-Order Theorem Proving</EM>, (Cork, Ireland),
     ENTCS, Elsevier Science

</DL>

<P>

<HR><!------------------------------------------------------------------------>


